(set-logic QF_BV)
(declare-fun x () (_ BitVec 2))
(declare-fun y () (_ BitVec 1))
(declare-fun z () Bool)
(assert 
(let ((e9 (concat (_ bv0 2) y))) 
(let ((e20 (bvsge e9 ((_ sign_extend 1) x)))) 
(let ((e21 (bvuge (_ bv0 1) y))) 
(let ((e22 (bvsgt (_ bv0 2) x))) 
(let ((e24 (= x (_ bv0 2)))) 
(let ((e26 (bvsge (_ bv0 3) e9))) 
(let ((e29 (ite e20 e22 z))) 
(let ((e33 (xor e29 e21))) 
(let ((e39 (and e26 e24))) 
(let ((e40 (= e33 e39))) 
(let ((e46 (= e40 false))) 
(let ((e48 (xor e46 false))) e48)))))))))))))
(check-sat)

